D:Dsys, discrete:(IdId). d-feasible-discrete(D;discrete)   

latex

Definitions	Dsys, t  T, , Type, Id, x:AB(x), x:A. B(x), M(i), ma-ef-const(M;k;x;s;v), M.da(a), , M.state, Knd, ma-init-const(M;x), x:A  B(x), P & Q, f(a), b, P  Q, d-feasible-discrete(D;discrete)
Lemmas	assert wf, ma-init-const wf, Knd wf, ma-st wf, ma-da wf, ma-ef-const wf, d-m wf, Id wf, bool wf, dsys wf